LTL OR CTL

LTL OR CTL
==================

有个很大的争论 LTL更容易刻画安全属性，但是CTL更容易验证，因此哪个更合适呢？

• CTL限制了自己的表达能力和很多重要的行为，例如强fairness
• 但是另一方面CTL在验证时间上是线性增长的，而LTL会出现指数级增长的，因此在工业上用的比较多的还是CTL
• 但是CTL实在是有很多限制，例如它不兼容半形式化，可是LTL却可以，而且LTL可以很容易修改以便混合枚举和符号搜索算法
• LTL的复杂度是PSPACE-complete的